chore: bugfixes and benchmark code for the memory based simp_mem #218
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…m to fail if omega is taking too long.
…ck away from this change
…o so. Back away from this change" This reverts commit 01f5cde.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is a TODO, and has surprising interactions with Lean that I don't understand. I tried to cleanup the code to allow me to fix #154, but this lead to failures :( It's really unclear to me what's going to.
The key idea is this:
In the
simp_memtactic, I operate on it as aTacticM, usingrewriteto imperatively edit the main goal state. This causes successive rewrites in subexpressions to step over each other. Rather, I should be writing this inMetaM, wheresimp_memrecusively walks the expression, and optionally rewrites it with one of the visitor patterns. This is a fairly large-scale change. and I was hoping that I could perform this change, which also using the opportunity to eliminate my uses ofevalTactic. Unfortunately, that didn't happen, so I'm drafting this PR for now.